es:ES, k:Knd, e:E. es-kind-index(es;k;e)   

latex

Definitions	t  T, x:A. B(x), A  B, es-kind-index(es;k;e), n+m, a < b, Void, x:AB(x), P  Q, False, A, , {x:A| B(x)} , , pred(e), kind(e), a = b, , s = t, b, x:A  B(x), P & Q, P  Q, Unit, left + right, if b then t else f fi , #$n, b, , f(a), True, T, x:A. B(x), Knd, ES, i  j , -n, n - m, first(e), (e <loc e'), E, SWellFounded(R(x;y))
Lemmas	ge wf, nat properties, event system wf, Knd wf, es-axioms, nat wf, es-locl wf, es-E wf, bnot wf, not wf, assert wf, es-first wf, bool wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, eq knd wf, es-kind wf, es-pred wf, le wf